(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


(** ** The Properties of Matrix Transpose *)

Require Import List.
Require Import Matrix.Mat.Mat_def.
Require Import Matrix.Mat.list_function.
Require Import Matrix.Mat.Mat_IO.
Require Import Matrix.Mat.Mat_map.
Require Import Matrix.Mat.Mat_trans.
Require Import Matrix.Mat.Mat_mult.
Require Import Matrix.Mat.Mat_mult_lemma.

(* ################################################################# *)
(** * Basic Properties of Single Matrix Transpose *)

Section Mstrans_lemma.
Variable A:Set.
Variable Zero:A.
Variable add:A->A->A.
Variable mul:A->A->A.

(** ** The Matrix is equal to itself after two transpose operations :
       T(T(A)) = A *)

(** *** trans_same *)
(** Two-dimensional list is equal to itself after two gettrans
    operations. *)
Lemma trans_same : forall ma m n , 
    height ma = m-> width ma n  ->
    gettrans A Zero (gettrans A Zero ma n) m = ma.
Proof.
induction ma as [|x' mma' IHma'].
- simpl. intros. rewrite <- H. simpl. auto.
- induction m as [|m' IHm']. 
  + simpl. intros. inversion H.
  + simpl. intros. destruct H0.
    induction n as [|n' IHn'].
      { simpl. rewrite length_zero_iff_nil in H0. rewrite H0. f_equal.
        apply gettrans_nil'. auto. auto. }
      { intros. rewrite <- link_gettrans with (m:=m').
       rewrite headcolumn_link with (m:=S n').
       rewrite tailcolumn_link with (m:=S n').
       rewrite IHma'. simpl. f_equal.
       inversion H. auto. apply H1.
        inversion H0. auto.
        apply height_gettrans. auto.
        apply height_gettrans. auto.
        inversion H. auto. apply H1.
      } 
Qed.

(** ** tteq *)
(** The matrix is equal to itself after two gettrans operations. *)
Lemma tteq : forall {m n:nat} (ma:@Mat A m n) ,
  trans A Zero (trans A Zero ma) === ma.
Proof.
  intros.
  unfold M_eq.
  simpl.
  induction ma.
  simpl.
  apply trans_same;auto.
Qed.


(** ** The Property of Multiplication and Transpose of Constant and Matrix*)



(** *** c_mul_dl_nil_list *)
(** Multiplication properties of constant and nil equals to nil_list. *)
Lemma c_mul_dl_nil_list: forall {c:A} 
  (n:nat),
  c_mul_dl A mul c (nil_list A n) = nil_list A n.
Proof.
  induction n.
  - simpl. reflexivity.
  - simpl. f_equal. apply IHn.
Qed.

(** *** c_mul_l_head *)
(** The relationship between head and get_mul_c_v. *)
Lemma c_mul_l_head: forall a (l:list A),
  (forall a ,mul a Zero = Zero) ->
  @hd A Zero (c_mul_l A mul a l) = mul a (@hd A Zero l).
Proof.
  induction l.
  - intros. simpl. rewrite H. reflexivity.
  - intros. simpl. reflexivity.
Qed.

(** *** c_mul_dl_headcolumn *)
(** The relationship between headcolumn and get_mul_c_v. *)
Lemma c_mul_dl_headcolumn : forall c ma,
  (forall a ,mul a Zero = Zero) ->
  headcolumn A Zero (c_mul_dl A mul c ma) =
  c_mul_l A mul c (headcolumn A Zero ma).
Proof.
  induction ma.
  - simpl. reflexivity.
  - intros. simpl. rewrite c_mul_l_head. f_equal.
    apply IHma. apply H. apply H.
Qed.


(** *** c_mul_dl_cons *)
Lemma c_mul_dl_cons : forall {c:A} (a:list A)(ma:list(list A)),
  c_mul_dl A mul c (a::ma) = (c_mul_l A mul c a)::(c_mul_dl A mul c ma).
Proof.
  induction ma.
  - simpl. reflexivity.
  - simpl. f_equal.
Qed.

(** *** c_mul_dl_link *)
(** The relationship between get_mul_c_m' and link. *)
Lemma c_mul_dl_link : forall {c:A} m (a:list A)(ma:list(list A)), 
  length a=m -> length ma = m->
  c_mul_dl A mul c (link A a ma) 
  = link A ( c_mul_l A mul c a) (c_mul_dl A mul c ma).
Proof.
  induction m.
  - induction a.
    + simpl. auto.
    + intros. inversion H. 
  - induction a. 
    + intros. inversion H.
    + intros. induction ma.
      * simpl. auto.
      * simpl. f_equal. apply IHm. inversion H. auto.
        inversion H0. auto.
Qed.

(** ctrans_same_l *)
(** The transposed property of the constant multiplied by two-dimensional
    list. *)
Lemma ctrans_same:forall(m n:nat) c (ma: list(list A)),
  (height ma = m) -> (width ma n) ->
  (forall a ,mul a Zero = Zero) ->
  gettrans A Zero (c_mul_dl A mul c ma) n
  = c_mul_dl A mul c (gettrans A Zero ma n).
Proof.
  induction m.
  - induction n.
    + induction ma.
      * simpl. auto.
      * intros. inversion H.
    + induction ma.
      * intros. simpl. f_equal. rewrite ?gettrans_nil.
        rewrite c_mul_dl_nil_list. reflexivity.
      * intros. inversion H.
  - induction n.
    + induction ma.
      * intros. inversion H.
      * simpl. auto.
    + induction ma.
      * intros. inversion H.
      * intros. rewrite c_mul_dl_cons.
        rewrite <- ?link_gettrans with (m:=m ).
        rewrite c_mul_dl_link with(m0:= S n).
        f_equal. apply IHm. inversion H. auto.
        inversion H0. apply H3. apply H1. inversion H0.
        apply H2. apply height_gettrans. inversion H0.
        apply H2. inversion H. auto. inversion H0. apply H3.
        rewrite length_c_mul_l. inversion H0. apply H2.
        rewrite height_c_mul_dl. inversion H. auto.
        apply width_c_mul_dl. inversion H0. apply H3.
Qed.

(** ** cteq*)
(** The transposed property of the constant multiplied by matrix :
    T(c*A) = c*T(A). *)
Lemma cteq : forall{m n:nat} c (ma:@Mat A m n),
  (forall a ,mul a Zero = Zero) ->
  trans A Zero ( const_mul_l A mul c ma)
  === const_mul_l A mul c (trans A Zero ma).
Proof.
  unfold M_eq. simpl. unfold trans,c_mul_mat. simpl.
  intros. rewrite ctrans_same with (m:= m)(n:=n).
  reflexivity. apply (mat_height A m n ma). apply (mat_width A m n ma).
  apply H.
Qed.

(** * Basic Properties of Multiple Matrices Transpose *)

(** ** meq_teq *)
(** if A = B then T(A) = T(B). **)
Lemma meq_teq : forall {m n:nat} (ma mb:@Mat A m n),
  (ma === mb) <-> trans A Zero ma === trans A Zero mb.
Proof.
  split.
  - intros. unfold M_eq. unfold trans. simpl. rewrite H. reflexivity.
  - intros. rewrite <- tteq with(ma0:=ma). rewrite <- tteq with (ma0:=mb).
    unfold trans,M_eq in H. simpl in H.
    unfold trans,M_eq . simpl.
    rewrite H. reflexivity.
Qed.


(** ** teq_add *)
(** Transpose properties of matrix addition : T(A+B) =T(A) +T(B) *)
Lemma teq_add : forall {m n:nat} (ma mb:@Mat A m n),
  (forall a , add a Zero = a) ->
  trans A Zero (matrix_each A add ma mb ) 
  === matrix_each A add  (trans A Zero ma ) (trans A Zero mb).
Proof.
  unfold M_eq. unfold trans,matrix_each,mat_each. simpl.
  intros. rewrite gettrans_mat_each' with(m:= m). auto.
  apply (mat_height A m n ma). apply (mat_height A m n mb).
  apply (mat_width A m n ma). apply (mat_width A m n mb).
  apply H.
Qed.

(** ** teq_mul *)
(** Transpose properties of matrix multiplication : T(AB) = T(B)*T(A) *)
Lemma teq_mul : forall {m n p:nat} (ma:@Mat A m n)(mb:@Mat A n p),
  (forall a , add Zero a = a) ->(forall a b : A, mul a b = mul b a) ->
  trans A Zero (matrix_mul A Zero add mul ma mb ) 
  === matrix_mul A Zero add mul (trans A Zero mb ) (trans A Zero ma).
Proof.
  unfold M_eq. unfold trans, matrix_mul,mat_mul_mat.
  simpl. intros. rewrite trans_same with (ma:=(mat A m n ma)).
  rewrite dl_mul_dl_gettrans_r with(m:=m)(n:=n)(p:=p). rewrite trans_same.
  reflexivity. auto. rewrite height_dl_mul_dl. rewrite height_gettrans.
  auto. apply width_dl_mul_dl. apply(mat_height A m n ma).
  apply H0. apply(mat_height A m n ma). apply(mat_width A m n ma).
  apply(mat_height A n p mb). apply(mat_width A n p mb). auto.
  apply(mat_height A m n ma). apply(mat_width A m n ma).
Qed.
Variable One:A.
(** ** matrix_mul_unit_l **)
(** The multplication of a unit matrix and a matrix equals to the matrix
    itself : I * ma = ma. *)
Lemma matrix_mul_unit_r : forall {m n:nat} (ma:@Mat A m n),
  (forall a,mul One a = a) ->
  (forall a,add a Zero = a) ->
  (forall a,mul Zero a = Zero)->
  (forall a,add Zero a = a) ->
  (forall a b, mul a b = mul b a)->
  matrix_mul A Zero add mul ma (MI A Zero One n) === ma.
Proof.
  intros. apply meq_teq. rewrite teq_mul.
  rewrite trans_MI. rewrite matrix_mul_unit_l. unfold trans,M_eq.
  simpl. auto. auto. auto. auto. auto. auto. auto.
Qed.

End Mstrans_lemma.